$\forall$$A$, $B$:Type, $L$:(($A$$\rightarrow$($B$ + Top)) List), $f$:($A$$\rightarrow$($B$ + Top)).
\\[0ex]p{-}first([$f$ / $L$]) = [$f$?p{-}first($L$)] $\in$ $A$$\rightarrow$($B$ + Top)